$\forall$$i$,$a$:Id, ${\it es}$:event\_system\{i:l\}. @$i$ locl($a$) occurs once $\in$ prop\{i:l\}